*****TAUT ∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B) rw,59;

60 ∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B)  

*****∃E ↑ w1;

61 A(RW,w1,W2,0)∧color(W2,w1)=B  (61)

*****∀E foolscap w3;

62 color(W123,w3)=W  

*****∀E foolscap w1;

63 color(W123,w1)=W  

*****∀E foolscap RW;

64 color(W123,RW)=W  

*****TAUTEQ A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1) 62:63;

65 A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1)  

*****∀I ↑ w3;

66 ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1))  

*****TAUTEQ A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW) 62,64;

67 A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW)  

*****∀I ↑ w3;

68 ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW))  

*****TAUT ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1))≡∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW)%
) 66,68;

69 ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1))≡∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW))  

*****ASSUME p=W123;

70 p=W123  (70)

*****SUBST ↑ IN ↑↑;

71 ∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,RW))  (70)

*****⊃I ↑↑⊃↑;

72 p=W123⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,RW)))  

*****∀E initial1 B,RW;

73 A(RW,RW,W123,0)⊃(((B=W∨(color(W2,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B))∧(((B=W∨(color(W1,%
RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B))∧((B=W∨(color(W1,RW)=W∨color(W2,RW)=W))⊃∃w1.(A(RW,w1,W%
3,0)∧color(W3,w1)=B))))  

*****TAUTEQ ∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B) rw,26,73;

74 ∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B)  

*****∃E ↑ w1;

75 A(RW,w1,W1,0)∧color(W1,w1)=B  (75)

*****TAUTEQ ¬(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) rw,color1,75;

76 ¬(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW))  (75)

*****∃I ↑ w1 ;

77 ∃w1.¬(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW))  

*****UNIFY ¬∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) ↑;

78 ¬∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW))  

*****TAUTEQ ∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B) rw,color1,26,73;

79 ∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B)  

*****∃E ↑ w1;

80 A(RW,w1,W2,0)∧color(W2,w1)=B  (80)

*****TAUTEQ ¬(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW)) rw,color1,80;

81 ¬(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW))  (80)

*****∃I ↑ w1 ;

82 ∃w1.¬(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW))  

*****UNIFY ¬∀w1.(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW)) ↑;

83 ¬∀w1.(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW))  

*****TAUTEQ ∃w1.(A(RW,w1,W3,0)∧color(W3,w1)=B) rw,color1,26,73;

84 ∃w1.(A(RW,w1,W3,0)∧color(W3,w1)=B)  

*****∃E ↑ w1;

85 A(RW,w1,W3,0)∧color(W3,w1)=B  (85)

*****TAUTEQ ¬(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW)) rw,color1,85;

86 ¬(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW))  (85)

*****∃I ↑ w1 ;

87 ∃w1.¬(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW))  

*****UNIFY ¬∀w1.(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW)) ↑;

88 ¬∀w1.(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW))  

*****∀E w123 RW,w1,0;

89 (A(RW,w1,W1,0)∨(A(RW,w1,W2,0)∨A(RW,w1,W3,0)))⊃A(RW,w1,W123,0)  

*****TAUT A(RW,w1,W123,0) 61,89;

90 A(RW,w1,W123,0)  (61)

*****∀E initial3 RW,w1;

91 (A(RW,RW,W123,0)∧A(RW,w1,W2,0))⊃(color(W1,w1)=color(W1,RW)∧color(W3,w1)=color(W3,RW))  

*****TAUTEQ color(W1,w1)=W∧color(W3,w1)=W rw,26,61,91;

92 color(W1,w1)=W∧color(W3,w1)=W  (61)

*****∀E initial1 B,w1;

93 A(RW,w1,W123,0)⊃(((B=W∨(color(W2,w1)=W∨color(W3,w1)=W))⊃∃w.(A(w1,w,W1,0)∧color(W1,w)=B))∧(((B=W∨(color(W1,w1)%
=W∨color(W3,w1)=W))⊃∃w.(A(w1,w,W2,0)∧color(W2,w)=B))∧((B=W∨(color(W1,w1)=W∨color(W2,w1)=W))⊃∃w.(A(w1,w,W3,0)∧col%
or(W3,w)=B))))  

*****TAUTEQ ∃w.(A(w1,w,W1,0)∧color(W1,w)=B) 90,92:93;

94 ∃w.(A(w1,w,W1,0)∧color(W1,w)=B)  (61)

*****∃E ↑ w3;

95 A(w1,w3,W1,0)∧color(W1,w3)=B  (95)

*****TAUTEQ ¬(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1)) color1,92,95;

96 ¬(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1))  (61 95)

*****∃I ↑ w3 ;

97 ∃w3.¬(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1))  (61)

*****UNIFY ¬∀w3.(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1)) ↑;

98 ¬∀w3.(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1))  (61)